Issue1228.agda:40,1-45
Use def instead of con for non-constructor tt
